T:Type, l:IdLnk, ds1, ds2:x:Id fp Type, P:(State(ds1)Prop), Q:(State(ds2)Prop),
f:(State(ds1)T).
Normal(T)
 Normal(ds1)
 Normal(ds2)
 (s:State(ds1). Dec(k:. P(s,k)))
 (s:State(ds2). Dec(k:. Q(s,k)))
 (s:State(ds1), k:. Dec(P(s,k)))
 (s:State(ds2), k:. Dec(Q(s,k)))
 sendMinimalR{a:ut2, tg:ut2}(T; l; ds1; ds2; P; Q; f)  Realizer 

latex

Definitions	Normal(T), P  Q, False, A & B, x:A. B(x), AB, , sendMinimalR{$a:ut2, $tg:ut2}(T; l; ds1; ds2; P; Q; f), x(s1,s2), x:A. B(x), Prop, A, x. t(x), P & Q, t  T, Id, x(s), State(ds), IdLnk, a:A fp B(a)
Lemmas	normal-ds wf, normal-type wf, decidable wf, IdLnk wf, Rlist wf, decidable-min-lemma, Id wf, decl-state wf, fpf wf, weakPrecondSendR wf, nat wf, le wf, not wf